ackin(s(X), s(Y)) → u21(ackin(s(X), Y), X)
u21(ackout(X), Y) → u22(ackin(Y, X))
↳ QTRS
↳ DependencyPairsProof
ackin(s(X), s(Y)) → u21(ackin(s(X), Y), X)
u21(ackout(X), Y) → u22(ackin(Y, X))
ACKIN(s(X), s(Y)) → ACKIN(s(X), Y)
U21(ackout(X), Y) → ACKIN(Y, X)
ACKIN(s(X), s(Y)) → U21(ackin(s(X), Y), X)
ackin(s(X), s(Y)) → u21(ackin(s(X), Y), X)
u21(ackout(X), Y) → u22(ackin(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ACKIN(s(X), s(Y)) → ACKIN(s(X), Y)
U21(ackout(X), Y) → ACKIN(Y, X)
ACKIN(s(X), s(Y)) → U21(ackin(s(X), Y), X)
ackin(s(X), s(Y)) → u21(ackin(s(X), Y), X)
u21(ackout(X), Y) → u22(ackin(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
ACKIN(s(X), s(Y)) → ACKIN(s(X), Y)
ackin(s(X), s(Y)) → u21(ackin(s(X), Y), X)
u21(ackout(X), Y) → u22(ackin(Y, X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACKIN(s(X), s(Y)) → ACKIN(s(X), Y)
The value of delta used in the strict ordering is 4.
POL(ACKIN(x1, x2)) = (4)x_2
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
ackin(s(X), s(Y)) → u21(ackin(s(X), Y), X)
u21(ackout(X), Y) → u22(ackin(Y, X))